Termination w.r.t. Q proof of TRS/secret05cime5.trs

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

intersect'ii'in₂(cons₂(X, X0), cons₂(X, X1)) -> intersect'ii'out
intersect'ii'in₂(Xs, cons₂(X0, Ys)) -> u'1'1₁(intersect'ii'in₂(Xs, Ys))
u'1'1₁(intersect'ii'out) -> intersect'ii'out
intersect'ii'in₂(cons₂(X0, Xs), Ys) -> u'2'1₁(intersect'ii'in₂(Xs, Ys))
u'2'1₁(intersect'ii'out) -> intersect'ii'out
reduce'ii'in₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> u'3'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF))
u'3'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(iff₂(A, B), Fs), Gs), NF) -> u'4'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Fs), Gs), NF))
u'4'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2a₂(F1, F2), Fs), Gs), NF) -> u'5'1₁(reduce'ii'in₂(sequent₂(cons₂(F1, cons₂(F2, Fs)), Gs), NF))
u'5'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2b₂(F1, F2), Fs), Gs), NF) -> u'6'1₅(reduce'ii'in₂(sequent₂(cons₂(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1₅(reduce'ii'out, F2, Fs, Gs, NF) -> u'6'2₁(reduce'ii'in₂(sequent₂(cons₂(F2, Fs), Gs), NF))
u'6'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2d₁(F1), Fs), Gs), NF) -> u'7'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(F1, Gs)), NF))
u'7'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> u'8'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF))
u'8'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(iff₂(A, B), Gs)), NF) -> u'9'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Gs)), NF))
u'9'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(p₁(V), Fs), Gs), sequent₂(Left, Right)) -> u'10'1₁(reduce'ii'in₂(sequent₂(Fs, Gs), sequent₂(cons₂(p₁(V), Left), Right)))
u'10'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(G1, G2), Gs)), NF) -> u'11'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, cons₂(G2, Gs))), NF))
u'11'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(G1, G2), Gs)), NF) -> u'12'1₅(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1₅(reduce'ii'out, Fs, G2, Gs, NF) -> u'12'2₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G2, Gs)), NF))
u'12'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2d₁(G1), Gs)), NF) -> u'13'1₁(reduce'ii'in₂(sequent₂(cons₂(G1, Fs), Gs), NF))
u'13'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, cons₂(p₁(V), Gs)), sequent₂(Left, Right)) -> u'14'1₁(reduce'ii'in₂(sequent₂(nil, Gs), sequent₂(Left, cons₂(p₁(V), Right))))
u'14'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, nil), sequent₂(F1, F2)) -> u'15'1₁(intersect'ii'in₂(F1, F2))
u'15'1₁(intersect'ii'out) -> reduce'ii'out
tautology'i'in₁(F) -> u'16'1₁(reduce'ii'in₂(sequent₂(nil, cons₂(F, nil)), sequent₂(nil, nil)))
u'16'1₁(reduce'ii'out) -> tautology'i'out

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

intersect'ii'in₂(cons₂(X, X0), cons₂(X, X1)) -> intersect'ii'out
intersect'ii'in₂(Xs, cons₂(X0, Ys)) -> u'1'1₁(intersect'ii'in₂(Xs, Ys))
u'1'1₁(intersect'ii'out) -> intersect'ii'out
intersect'ii'in₂(cons₂(X0, Xs), Ys) -> u'2'1₁(intersect'ii'in₂(Xs, Ys))
u'2'1₁(intersect'ii'out) -> intersect'ii'out
reduce'ii'in₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> u'3'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF))
u'3'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(iff₂(A, B), Fs), Gs), NF) -> u'4'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Fs), Gs), NF))
u'4'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2a₂(F1, F2), Fs), Gs), NF) -> u'5'1₁(reduce'ii'in₂(sequent₂(cons₂(F1, cons₂(F2, Fs)), Gs), NF))
u'5'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2b₂(F1, F2), Fs), Gs), NF) -> u'6'1₅(reduce'ii'in₂(sequent₂(cons₂(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1₅(reduce'ii'out, F2, Fs, Gs, NF) -> u'6'2₁(reduce'ii'in₂(sequent₂(cons₂(F2, Fs), Gs), NF))
u'6'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2d₁(F1), Fs), Gs), NF) -> u'7'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(F1, Gs)), NF))
u'7'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> u'8'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF))
u'8'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(iff₂(A, B), Gs)), NF) -> u'9'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Gs)), NF))
u'9'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(p₁(V), Fs), Gs), sequent₂(Left, Right)) -> u'10'1₁(reduce'ii'in₂(sequent₂(Fs, Gs), sequent₂(cons₂(p₁(V), Left), Right)))
u'10'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(G1, G2), Gs)), NF) -> u'11'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, cons₂(G2, Gs))), NF))
u'11'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(G1, G2), Gs)), NF) -> u'12'1₅(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1₅(reduce'ii'out, Fs, G2, Gs, NF) -> u'12'2₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G2, Gs)), NF))
u'12'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2d₁(G1), Gs)), NF) -> u'13'1₁(reduce'ii'in₂(sequent₂(cons₂(G1, Fs), Gs), NF))
u'13'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, cons₂(p₁(V), Gs)), sequent₂(Left, Right)) -> u'14'1₁(reduce'ii'in₂(sequent₂(nil, Gs), sequent₂(Left, cons₂(p₁(V), Right))))
u'14'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, nil), sequent₂(F1, F2)) -> u'15'1₁(intersect'ii'in₂(F1, F2))
u'15'1₁(intersect'ii'out) -> reduce'ii'out
tautology'i'in₁(F) -> u'16'1₁(reduce'ii'in₂(sequent₂(nil, cons₂(F, nil)), sequent₂(nil, nil)))
u'16'1₁(reduce'ii'out) -> tautology'i'out

Q is empty.

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2a₂(G1, G2), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(G1, Gs)), NF)
REDUCE'II'IN₂(sequent₂(cons₂(x'2d₁(F1), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(F1, Gs)), NF)
REDUCE'II'IN₂(sequent₂(nil, nil), sequent₂(F1, F2)) -> U'15'1₁(intersect'ii'in₂(F1, F2))
REDUCE'II'IN₂(sequent₂(cons₂(x'2a₂(F1, F2), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(F1, cons₂(F2, Fs)), Gs), NF)
INTERSECT'II'IN₂(Xs, cons₂(X0, Ys)) -> U'1'1₁(intersect'ii'in₂(Xs, Ys))
REDUCE'II'IN₂(sequent₂(nil, cons₂(p₁(V), Gs)), sequent₂(Left, Right)) -> U'14'1₁(reduce'ii'in₂(sequent₂(nil, Gs), sequent₂(Left, cons₂(p₁(V), Right))))
REDUCE'II'IN₂(sequent₂(cons₂(x'2a₂(F1, F2), Fs), Gs), NF) -> U'5'1₁(reduce'ii'in₂(sequent₂(cons₂(F1, cons₂(F2, Fs)), Gs), NF))
U'12'1₅(reduce'ii'out, Fs, G2, Gs, NF) -> U'12'2₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G2, Gs)), NF))
REDUCE'II'IN₂(sequent₂(cons₂(x'2d₁(F1), Fs), Gs), NF) -> U'7'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(F1, Gs)), NF))
REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2a₂(G1, G2), Gs)), NF) -> U'12'1₅(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, Gs)), NF), Fs, G2, Gs, NF)
REDUCE'II'IN₂(sequent₂(cons₂(p₁(V), Fs), Gs), sequent₂(Left, Right)) -> REDUCE'II'IN₂(sequent₂(Fs, Gs), sequent₂(cons₂(p₁(V), Left), Right))
REDUCE'II'IN₂(sequent₂(cons₂(iff₂(A, B), Fs), Gs), NF) -> U'4'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Fs), Gs), NF))
REDUCE'II'IN₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> U'3'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF))
REDUCE'II'IN₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> U'8'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF))
REDUCE'II'IN₂(sequent₂(cons₂(x'2b₂(F1, F2), Fs), Gs), NF) -> U'6'1₅(reduce'ii'in₂(sequent₂(cons₂(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
INTERSECT'II'IN₂(Xs, cons₂(X0, Ys)) -> INTERSECT'II'IN₂(Xs, Ys)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2b₂(G1, G2), Gs)), NF) -> U'11'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, cons₂(G2, Gs))), NF))
REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2d₁(G1), Gs)), NF) -> U'13'1₁(reduce'ii'in₂(sequent₂(cons₂(G1, Fs), Gs), NF))
U'6'1₅(reduce'ii'out, F2, Fs, Gs, NF) -> REDUCE'II'IN₂(sequent₂(cons₂(F2, Fs), Gs), NF)
REDUCE'II'IN₂(sequent₂(nil, nil), sequent₂(F1, F2)) -> INTERSECT'II'IN₂(F1, F2)
REDUCE'II'IN₂(sequent₂(nil, cons₂(p₁(V), Gs)), sequent₂(Left, Right)) -> REDUCE'II'IN₂(sequent₂(nil, Gs), sequent₂(Left, cons₂(p₁(V), Right)))
REDUCE'II'IN₂(sequent₂(cons₂(p₁(V), Fs), Gs), sequent₂(Left, Right)) -> U'10'1₁(reduce'ii'in₂(sequent₂(Fs, Gs), sequent₂(cons₂(p₁(V), Left), Right)))
REDUCE'II'IN₂(sequent₂(cons₂(x'2b₂(F1, F2), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(F1, Fs), Gs), NF)
INTERSECT'II'IN₂(cons₂(X0, Xs), Ys) -> U'2'1₁(intersect'ii'in₂(Xs, Ys))
REDUCE'II'IN₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2d₁(G1), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(G1, Fs), Gs), NF)
INTERSECT'II'IN₂(cons₂(X0, Xs), Ys) -> INTERSECT'II'IN₂(Xs, Ys)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(iff₂(A, B), Gs)), NF) -> U'9'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Gs)), NF))
TAUTOLOGY'I'IN₁(F) -> REDUCE'II'IN₂(sequent₂(nil, cons₂(F, nil)), sequent₂(nil, nil))
REDUCE'II'IN₂(sequent₂(Fs, cons₂(iff₂(A, B), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Gs)), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2b₂(G1, G2), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(G1, cons₂(G2, Gs))), NF)
U'6'1₅(reduce'ii'out, F2, Fs, Gs, NF) -> U'6'2₁(reduce'ii'in₂(sequent₂(cons₂(F2, Fs), Gs), NF))
REDUCE'II'IN₂(sequent₂(cons₂(iff₂(A, B), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Fs), Gs), NF)
TAUTOLOGY'I'IN₁(F) -> U'16'1₁(reduce'ii'in₂(sequent₂(nil, cons₂(F, nil)), sequent₂(nil, nil)))
U'12'1₅(reduce'ii'out, Fs, G2, Gs, NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(G2, Gs)), NF)

The TRS R consists of the following rules:

intersect'ii'in₂(cons₂(X, X0), cons₂(X, X1)) -> intersect'ii'out
intersect'ii'in₂(Xs, cons₂(X0, Ys)) -> u'1'1₁(intersect'ii'in₂(Xs, Ys))
u'1'1₁(intersect'ii'out) -> intersect'ii'out
intersect'ii'in₂(cons₂(X0, Xs), Ys) -> u'2'1₁(intersect'ii'in₂(Xs, Ys))
u'2'1₁(intersect'ii'out) -> intersect'ii'out
reduce'ii'in₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> u'3'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF))
u'3'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(iff₂(A, B), Fs), Gs), NF) -> u'4'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Fs), Gs), NF))
u'4'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2a₂(F1, F2), Fs), Gs), NF) -> u'5'1₁(reduce'ii'in₂(sequent₂(cons₂(F1, cons₂(F2, Fs)), Gs), NF))
u'5'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2b₂(F1, F2), Fs), Gs), NF) -> u'6'1₅(reduce'ii'in₂(sequent₂(cons₂(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1₅(reduce'ii'out, F2, Fs, Gs, NF) -> u'6'2₁(reduce'ii'in₂(sequent₂(cons₂(F2, Fs), Gs), NF))
u'6'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2d₁(F1), Fs), Gs), NF) -> u'7'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(F1, Gs)), NF))
u'7'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> u'8'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF))
u'8'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(iff₂(A, B), Gs)), NF) -> u'9'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Gs)), NF))
u'9'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(p₁(V), Fs), Gs), sequent₂(Left, Right)) -> u'10'1₁(reduce'ii'in₂(sequent₂(Fs, Gs), sequent₂(cons₂(p₁(V), Left), Right)))
u'10'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(G1, G2), Gs)), NF) -> u'11'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, cons₂(G2, Gs))), NF))
u'11'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(G1, G2), Gs)), NF) -> u'12'1₅(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1₅(reduce'ii'out, Fs, G2, Gs, NF) -> u'12'2₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G2, Gs)), NF))
u'12'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2d₁(G1), Gs)), NF) -> u'13'1₁(reduce'ii'in₂(sequent₂(cons₂(G1, Fs), Gs), NF))
u'13'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, cons₂(p₁(V), Gs)), sequent₂(Left, Right)) -> u'14'1₁(reduce'ii'in₂(sequent₂(nil, Gs), sequent₂(Left, cons₂(p₁(V), Right))))
u'14'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, nil), sequent₂(F1, F2)) -> u'15'1₁(intersect'ii'in₂(F1, F2))
u'15'1₁(intersect'ii'out) -> reduce'ii'out
tautology'i'in₁(F) -> u'16'1₁(reduce'ii'in₂(sequent₂(nil, cons₂(F, nil)), sequent₂(nil, nil)))
u'16'1₁(reduce'ii'out) -> tautology'i'out

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2a₂(G1, G2), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(G1, Gs)), NF)
REDUCE'II'IN₂(sequent₂(cons₂(x'2d₁(F1), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(F1, Gs)), NF)
REDUCE'II'IN₂(sequent₂(nil, nil), sequent₂(F1, F2)) -> U'15'1₁(intersect'ii'in₂(F1, F2))
REDUCE'II'IN₂(sequent₂(cons₂(x'2a₂(F1, F2), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(F1, cons₂(F2, Fs)), Gs), NF)
INTERSECT'II'IN₂(Xs, cons₂(X0, Ys)) -> U'1'1₁(intersect'ii'in₂(Xs, Ys))
REDUCE'II'IN₂(sequent₂(nil, cons₂(p₁(V), Gs)), sequent₂(Left, Right)) -> U'14'1₁(reduce'ii'in₂(sequent₂(nil, Gs), sequent₂(Left, cons₂(p₁(V), Right))))
REDUCE'II'IN₂(sequent₂(cons₂(x'2a₂(F1, F2), Fs), Gs), NF) -> U'5'1₁(reduce'ii'in₂(sequent₂(cons₂(F1, cons₂(F2, Fs)), Gs), NF))
U'12'1₅(reduce'ii'out, Fs, G2, Gs, NF) -> U'12'2₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G2, Gs)), NF))
REDUCE'II'IN₂(sequent₂(cons₂(x'2d₁(F1), Fs), Gs), NF) -> U'7'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(F1, Gs)), NF))
REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2a₂(G1, G2), Gs)), NF) -> U'12'1₅(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, Gs)), NF), Fs, G2, Gs, NF)
REDUCE'II'IN₂(sequent₂(cons₂(p₁(V), Fs), Gs), sequent₂(Left, Right)) -> REDUCE'II'IN₂(sequent₂(Fs, Gs), sequent₂(cons₂(p₁(V), Left), Right))
REDUCE'II'IN₂(sequent₂(cons₂(iff₂(A, B), Fs), Gs), NF) -> U'4'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Fs), Gs), NF))
REDUCE'II'IN₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> U'3'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF))
REDUCE'II'IN₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> U'8'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF))
REDUCE'II'IN₂(sequent₂(cons₂(x'2b₂(F1, F2), Fs), Gs), NF) -> U'6'1₅(reduce'ii'in₂(sequent₂(cons₂(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
INTERSECT'II'IN₂(Xs, cons₂(X0, Ys)) -> INTERSECT'II'IN₂(Xs, Ys)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2b₂(G1, G2), Gs)), NF) -> U'11'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, cons₂(G2, Gs))), NF))
REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2d₁(G1), Gs)), NF) -> U'13'1₁(reduce'ii'in₂(sequent₂(cons₂(G1, Fs), Gs), NF))
U'6'1₅(reduce'ii'out, F2, Fs, Gs, NF) -> REDUCE'II'IN₂(sequent₂(cons₂(F2, Fs), Gs), NF)
REDUCE'II'IN₂(sequent₂(nil, nil), sequent₂(F1, F2)) -> INTERSECT'II'IN₂(F1, F2)
REDUCE'II'IN₂(sequent₂(nil, cons₂(p₁(V), Gs)), sequent₂(Left, Right)) -> REDUCE'II'IN₂(sequent₂(nil, Gs), sequent₂(Left, cons₂(p₁(V), Right)))
REDUCE'II'IN₂(sequent₂(cons₂(p₁(V), Fs), Gs), sequent₂(Left, Right)) -> U'10'1₁(reduce'ii'in₂(sequent₂(Fs, Gs), sequent₂(cons₂(p₁(V), Left), Right)))
REDUCE'II'IN₂(sequent₂(cons₂(x'2b₂(F1, F2), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(F1, Fs), Gs), NF)
INTERSECT'II'IN₂(cons₂(X0, Xs), Ys) -> U'2'1₁(intersect'ii'in₂(Xs, Ys))
REDUCE'II'IN₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2d₁(G1), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(G1, Fs), Gs), NF)
INTERSECT'II'IN₂(cons₂(X0, Xs), Ys) -> INTERSECT'II'IN₂(Xs, Ys)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(iff₂(A, B), Gs)), NF) -> U'9'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Gs)), NF))
TAUTOLOGY'I'IN₁(F) -> REDUCE'II'IN₂(sequent₂(nil, cons₂(F, nil)), sequent₂(nil, nil))
REDUCE'II'IN₂(sequent₂(Fs, cons₂(iff₂(A, B), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Gs)), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2b₂(G1, G2), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(G1, cons₂(G2, Gs))), NF)
U'6'1₅(reduce'ii'out, F2, Fs, Gs, NF) -> U'6'2₁(reduce'ii'in₂(sequent₂(cons₂(F2, Fs), Gs), NF))
REDUCE'II'IN₂(sequent₂(cons₂(iff₂(A, B), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Fs), Gs), NF)
TAUTOLOGY'I'IN₁(F) -> U'16'1₁(reduce'ii'in₂(sequent₂(nil, cons₂(F, nil)), sequent₂(nil, nil)))
U'12'1₅(reduce'ii'out, Fs, G2, Gs, NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(G2, Gs)), NF)

The TRS R consists of the following rules:

intersect'ii'in₂(cons₂(X, X0), cons₂(X, X1)) -> intersect'ii'out
intersect'ii'in₂(Xs, cons₂(X0, Ys)) -> u'1'1₁(intersect'ii'in₂(Xs, Ys))
u'1'1₁(intersect'ii'out) -> intersect'ii'out
intersect'ii'in₂(cons₂(X0, Xs), Ys) -> u'2'1₁(intersect'ii'in₂(Xs, Ys))
u'2'1₁(intersect'ii'out) -> intersect'ii'out
reduce'ii'in₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> u'3'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF))
u'3'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(iff₂(A, B), Fs), Gs), NF) -> u'4'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Fs), Gs), NF))
u'4'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2a₂(F1, F2), Fs), Gs), NF) -> u'5'1₁(reduce'ii'in₂(sequent₂(cons₂(F1, cons₂(F2, Fs)), Gs), NF))
u'5'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2b₂(F1, F2), Fs), Gs), NF) -> u'6'1₅(reduce'ii'in₂(sequent₂(cons₂(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1₅(reduce'ii'out, F2, Fs, Gs, NF) -> u'6'2₁(reduce'ii'in₂(sequent₂(cons₂(F2, Fs), Gs), NF))
u'6'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2d₁(F1), Fs), Gs), NF) -> u'7'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(F1, Gs)), NF))
u'7'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> u'8'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF))
u'8'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(iff₂(A, B), Gs)), NF) -> u'9'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Gs)), NF))
u'9'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(p₁(V), Fs), Gs), sequent₂(Left, Right)) -> u'10'1₁(reduce'ii'in₂(sequent₂(Fs, Gs), sequent₂(cons₂(p₁(V), Left), Right)))
u'10'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(G1, G2), Gs)), NF) -> u'11'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, cons₂(G2, Gs))), NF))
u'11'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(G1, G2), Gs)), NF) -> u'12'1₅(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1₅(reduce'ii'out, Fs, G2, Gs, NF) -> u'12'2₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G2, Gs)), NF))
u'12'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2d₁(G1), Gs)), NF) -> u'13'1₁(reduce'ii'in₂(sequent₂(cons₂(G1, Fs), Gs), NF))
u'13'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, cons₂(p₁(V), Gs)), sequent₂(Left, Right)) -> u'14'1₁(reduce'ii'in₂(sequent₂(nil, Gs), sequent₂(Left, cons₂(p₁(V), Right))))
u'14'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, nil), sequent₂(F1, F2)) -> u'15'1₁(intersect'ii'in₂(F1, F2))
u'15'1₁(intersect'ii'out) -> reduce'ii'out
tautology'i'in₁(F) -> u'16'1₁(reduce'ii'in₂(sequent₂(nil, cons₂(F, nil)), sequent₂(nil, nil)))
u'16'1₁(reduce'ii'out) -> tautology'i'out

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 2 SCCs with 18 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

INTERSECT'II'IN₂(cons₂(X0, Xs), Ys) -> INTERSECT'II'IN₂(Xs, Ys)
INTERSECT'II'IN₂(Xs, cons₂(X0, Ys)) -> INTERSECT'II'IN₂(Xs, Ys)

The TRS R consists of the following rules:

intersect'ii'in₂(cons₂(X, X0), cons₂(X, X1)) -> intersect'ii'out
intersect'ii'in₂(Xs, cons₂(X0, Ys)) -> u'1'1₁(intersect'ii'in₂(Xs, Ys))
u'1'1₁(intersect'ii'out) -> intersect'ii'out
intersect'ii'in₂(cons₂(X0, Xs), Ys) -> u'2'1₁(intersect'ii'in₂(Xs, Ys))
u'2'1₁(intersect'ii'out) -> intersect'ii'out
reduce'ii'in₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> u'3'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF))
u'3'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(iff₂(A, B), Fs), Gs), NF) -> u'4'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Fs), Gs), NF))
u'4'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2a₂(F1, F2), Fs), Gs), NF) -> u'5'1₁(reduce'ii'in₂(sequent₂(cons₂(F1, cons₂(F2, Fs)), Gs), NF))
u'5'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2b₂(F1, F2), Fs), Gs), NF) -> u'6'1₅(reduce'ii'in₂(sequent₂(cons₂(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1₅(reduce'ii'out, F2, Fs, Gs, NF) -> u'6'2₁(reduce'ii'in₂(sequent₂(cons₂(F2, Fs), Gs), NF))
u'6'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2d₁(F1), Fs), Gs), NF) -> u'7'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(F1, Gs)), NF))
u'7'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> u'8'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF))
u'8'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(iff₂(A, B), Gs)), NF) -> u'9'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Gs)), NF))
u'9'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(p₁(V), Fs), Gs), sequent₂(Left, Right)) -> u'10'1₁(reduce'ii'in₂(sequent₂(Fs, Gs), sequent₂(cons₂(p₁(V), Left), Right)))
u'10'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(G1, G2), Gs)), NF) -> u'11'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, cons₂(G2, Gs))), NF))
u'11'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(G1, G2), Gs)), NF) -> u'12'1₅(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1₅(reduce'ii'out, Fs, G2, Gs, NF) -> u'12'2₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G2, Gs)), NF))
u'12'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2d₁(G1), Gs)), NF) -> u'13'1₁(reduce'ii'in₂(sequent₂(cons₂(G1, Fs), Gs), NF))
u'13'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, cons₂(p₁(V), Gs)), sequent₂(Left, Right)) -> u'14'1₁(reduce'ii'in₂(sequent₂(nil, Gs), sequent₂(Left, cons₂(p₁(V), Right))))
u'14'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, nil), sequent₂(F1, F2)) -> u'15'1₁(intersect'ii'in₂(F1, F2))
u'15'1₁(intersect'ii'out) -> reduce'ii'out
tautology'i'in₁(F) -> u'16'1₁(reduce'ii'in₂(sequent₂(nil, cons₂(F, nil)), sequent₂(nil, nil)))
u'16'1₁(reduce'ii'out) -> tautology'i'out

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

INTERSECT'II'IN₂(Xs, cons₂(X0, Ys)) -> INTERSECT'II'IN₂(Xs, Ys)

The remaining pairs can at least be oriented weakly.

INTERSECT'II'IN₂(cons₂(X0, Xs), Ys) -> INTERSECT'II'IN₂(Xs, Ys)

Used ordering: Polynomial Order [17,21] with Interpretation:

POL( cons₂(x₁, x₂) ) = 3x₁ + 2x₂ + 1

POL( INTERSECT'II'IN₂(x₁, x₂) ) = 3x₂ + 2

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

INTERSECT'II'IN₂(cons₂(X0, Xs), Ys) -> INTERSECT'II'IN₂(Xs, Ys)

The TRS R consists of the following rules:

intersect'ii'in₂(cons₂(X, X0), cons₂(X, X1)) -> intersect'ii'out
intersect'ii'in₂(Xs, cons₂(X0, Ys)) -> u'1'1₁(intersect'ii'in₂(Xs, Ys))
u'1'1₁(intersect'ii'out) -> intersect'ii'out
intersect'ii'in₂(cons₂(X0, Xs), Ys) -> u'2'1₁(intersect'ii'in₂(Xs, Ys))
u'2'1₁(intersect'ii'out) -> intersect'ii'out
reduce'ii'in₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> u'3'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF))
u'3'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(iff₂(A, B), Fs), Gs), NF) -> u'4'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Fs), Gs), NF))
u'4'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2a₂(F1, F2), Fs), Gs), NF) -> u'5'1₁(reduce'ii'in₂(sequent₂(cons₂(F1, cons₂(F2, Fs)), Gs), NF))
u'5'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2b₂(F1, F2), Fs), Gs), NF) -> u'6'1₅(reduce'ii'in₂(sequent₂(cons₂(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1₅(reduce'ii'out, F2, Fs, Gs, NF) -> u'6'2₁(reduce'ii'in₂(sequent₂(cons₂(F2, Fs), Gs), NF))
u'6'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2d₁(F1), Fs), Gs), NF) -> u'7'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(F1, Gs)), NF))
u'7'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> u'8'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF))
u'8'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(iff₂(A, B), Gs)), NF) -> u'9'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Gs)), NF))
u'9'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(p₁(V), Fs), Gs), sequent₂(Left, Right)) -> u'10'1₁(reduce'ii'in₂(sequent₂(Fs, Gs), sequent₂(cons₂(p₁(V), Left), Right)))
u'10'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(G1, G2), Gs)), NF) -> u'11'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, cons₂(G2, Gs))), NF))
u'11'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(G1, G2), Gs)), NF) -> u'12'1₅(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1₅(reduce'ii'out, Fs, G2, Gs, NF) -> u'12'2₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G2, Gs)), NF))
u'12'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2d₁(G1), Gs)), NF) -> u'13'1₁(reduce'ii'in₂(sequent₂(cons₂(G1, Fs), Gs), NF))
u'13'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, cons₂(p₁(V), Gs)), sequent₂(Left, Right)) -> u'14'1₁(reduce'ii'in₂(sequent₂(nil, Gs), sequent₂(Left, cons₂(p₁(V), Right))))
u'14'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, nil), sequent₂(F1, F2)) -> u'15'1₁(intersect'ii'in₂(F1, F2))
u'15'1₁(intersect'ii'out) -> reduce'ii'out
tautology'i'in₁(F) -> u'16'1₁(reduce'ii'in₂(sequent₂(nil, cons₂(F, nil)), sequent₂(nil, nil)))
u'16'1₁(reduce'ii'out) -> tautology'i'out

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

INTERSECT'II'IN₂(cons₂(X0, Xs), Ys) -> INTERSECT'II'IN₂(Xs, Ys)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial Order [17,21] with Interpretation:

POL( cons₂(x₁, x₂) ) = 2x₂ + 1

POL( INTERSECT'II'IN₂(x₁, x₂) ) = x₁ + 3

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ PisEmptyProof

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

intersect'ii'in₂(cons₂(X, X0), cons₂(X, X1)) -> intersect'ii'out
intersect'ii'in₂(Xs, cons₂(X0, Ys)) -> u'1'1₁(intersect'ii'in₂(Xs, Ys))
u'1'1₁(intersect'ii'out) -> intersect'ii'out
intersect'ii'in₂(cons₂(X0, Xs), Ys) -> u'2'1₁(intersect'ii'in₂(Xs, Ys))
u'2'1₁(intersect'ii'out) -> intersect'ii'out
reduce'ii'in₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> u'3'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF))
u'3'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(iff₂(A, B), Fs), Gs), NF) -> u'4'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Fs), Gs), NF))
u'4'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2a₂(F1, F2), Fs), Gs), NF) -> u'5'1₁(reduce'ii'in₂(sequent₂(cons₂(F1, cons₂(F2, Fs)), Gs), NF))
u'5'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2b₂(F1, F2), Fs), Gs), NF) -> u'6'1₅(reduce'ii'in₂(sequent₂(cons₂(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1₅(reduce'ii'out, F2, Fs, Gs, NF) -> u'6'2₁(reduce'ii'in₂(sequent₂(cons₂(F2, Fs), Gs), NF))
u'6'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2d₁(F1), Fs), Gs), NF) -> u'7'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(F1, Gs)), NF))
u'7'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> u'8'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF))
u'8'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(iff₂(A, B), Gs)), NF) -> u'9'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Gs)), NF))
u'9'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(p₁(V), Fs), Gs), sequent₂(Left, Right)) -> u'10'1₁(reduce'ii'in₂(sequent₂(Fs, Gs), sequent₂(cons₂(p₁(V), Left), Right)))
u'10'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(G1, G2), Gs)), NF) -> u'11'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, cons₂(G2, Gs))), NF))
u'11'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(G1, G2), Gs)), NF) -> u'12'1₅(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1₅(reduce'ii'out, Fs, G2, Gs, NF) -> u'12'2₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G2, Gs)), NF))
u'12'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2d₁(G1), Gs)), NF) -> u'13'1₁(reduce'ii'in₂(sequent₂(cons₂(G1, Fs), Gs), NF))
u'13'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, cons₂(p₁(V), Gs)), sequent₂(Left, Right)) -> u'14'1₁(reduce'ii'in₂(sequent₂(nil, Gs), sequent₂(Left, cons₂(p₁(V), Right))))
u'14'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, nil), sequent₂(F1, F2)) -> u'15'1₁(intersect'ii'in₂(F1, F2))
u'15'1₁(intersect'ii'out) -> reduce'ii'out
tautology'i'in₁(F) -> u'16'1₁(reduce'ii'in₂(sequent₂(nil, cons₂(F, nil)), sequent₂(nil, nil)))
u'16'1₁(reduce'ii'out) -> tautology'i'out

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2a₂(G1, G2), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(G1, Gs)), NF)
REDUCE'II'IN₂(sequent₂(cons₂(x'2d₁(F1), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(F1, Gs)), NF)
REDUCE'II'IN₂(sequent₂(cons₂(x'2b₂(F1, F2), Fs), Gs), NF) -> U'6'1₅(reduce'ii'in₂(sequent₂(cons₂(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
U'6'1₅(reduce'ii'out, F2, Fs, Gs, NF) -> REDUCE'II'IN₂(sequent₂(cons₂(F2, Fs), Gs), NF)
REDUCE'II'IN₂(sequent₂(nil, cons₂(p₁(V), Gs)), sequent₂(Left, Right)) -> REDUCE'II'IN₂(sequent₂(nil, Gs), sequent₂(Left, cons₂(p₁(V), Right)))
REDUCE'II'IN₂(sequent₂(cons₂(x'2b₂(F1, F2), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(F1, Fs), Gs), NF)
REDUCE'II'IN₂(sequent₂(cons₂(x'2a₂(F1, F2), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(F1, cons₂(F2, Fs)), Gs), NF)
REDUCE'II'IN₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2d₁(G1), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(G1, Fs), Gs), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(iff₂(A, B), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Gs)), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2b₂(G1, G2), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(G1, cons₂(G2, Gs))), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2a₂(G1, G2), Gs)), NF) -> U'12'1₅(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, Gs)), NF), Fs, G2, Gs, NF)
REDUCE'II'IN₂(sequent₂(cons₂(iff₂(A, B), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Fs), Gs), NF)
REDUCE'II'IN₂(sequent₂(cons₂(p₁(V), Fs), Gs), sequent₂(Left, Right)) -> REDUCE'II'IN₂(sequent₂(Fs, Gs), sequent₂(cons₂(p₁(V), Left), Right))
U'12'1₅(reduce'ii'out, Fs, G2, Gs, NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(G2, Gs)), NF)

The TRS R consists of the following rules:

intersect'ii'in₂(cons₂(X, X0), cons₂(X, X1)) -> intersect'ii'out
intersect'ii'in₂(Xs, cons₂(X0, Ys)) -> u'1'1₁(intersect'ii'in₂(Xs, Ys))
u'1'1₁(intersect'ii'out) -> intersect'ii'out
intersect'ii'in₂(cons₂(X0, Xs), Ys) -> u'2'1₁(intersect'ii'in₂(Xs, Ys))
u'2'1₁(intersect'ii'out) -> intersect'ii'out
reduce'ii'in₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> u'3'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF))
u'3'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(iff₂(A, B), Fs), Gs), NF) -> u'4'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Fs), Gs), NF))
u'4'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2a₂(F1, F2), Fs), Gs), NF) -> u'5'1₁(reduce'ii'in₂(sequent₂(cons₂(F1, cons₂(F2, Fs)), Gs), NF))
u'5'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2b₂(F1, F2), Fs), Gs), NF) -> u'6'1₅(reduce'ii'in₂(sequent₂(cons₂(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1₅(reduce'ii'out, F2, Fs, Gs, NF) -> u'6'2₁(reduce'ii'in₂(sequent₂(cons₂(F2, Fs), Gs), NF))
u'6'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2d₁(F1), Fs), Gs), NF) -> u'7'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(F1, Gs)), NF))
u'7'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> u'8'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF))
u'8'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(iff₂(A, B), Gs)), NF) -> u'9'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Gs)), NF))
u'9'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(p₁(V), Fs), Gs), sequent₂(Left, Right)) -> u'10'1₁(reduce'ii'in₂(sequent₂(Fs, Gs), sequent₂(cons₂(p₁(V), Left), Right)))
u'10'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(G1, G2), Gs)), NF) -> u'11'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, cons₂(G2, Gs))), NF))
u'11'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(G1, G2), Gs)), NF) -> u'12'1₅(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1₅(reduce'ii'out, Fs, G2, Gs, NF) -> u'12'2₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G2, Gs)), NF))
u'12'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2d₁(G1), Gs)), NF) -> u'13'1₁(reduce'ii'in₂(sequent₂(cons₂(G1, Fs), Gs), NF))
u'13'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, cons₂(p₁(V), Gs)), sequent₂(Left, Right)) -> u'14'1₁(reduce'ii'in₂(sequent₂(nil, Gs), sequent₂(Left, cons₂(p₁(V), Right))))
u'14'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, nil), sequent₂(F1, F2)) -> u'15'1₁(intersect'ii'in₂(F1, F2))
u'15'1₁(intersect'ii'out) -> reduce'ii'out
tautology'i'in₁(F) -> u'16'1₁(reduce'ii'in₂(sequent₂(nil, cons₂(F, nil)), sequent₂(nil, nil)))
u'16'1₁(reduce'ii'out) -> tautology'i'out

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2a₂(G1, G2), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(G1, Gs)), NF)
REDUCE'II'IN₂(sequent₂(cons₂(x'2b₂(F1, F2), Fs), Gs), NF) -> U'6'1₅(reduce'ii'in₂(sequent₂(cons₂(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
U'6'1₅(reduce'ii'out, F2, Fs, Gs, NF) -> REDUCE'II'IN₂(sequent₂(cons₂(F2, Fs), Gs), NF)
REDUCE'II'IN₂(sequent₂(nil, cons₂(p₁(V), Gs)), sequent₂(Left, Right)) -> REDUCE'II'IN₂(sequent₂(nil, Gs), sequent₂(Left, cons₂(p₁(V), Right)))
REDUCE'II'IN₂(sequent₂(cons₂(x'2b₂(F1, F2), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(F1, Fs), Gs), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2a₂(G1, G2), Gs)), NF) -> U'12'1₅(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, Gs)), NF), Fs, G2, Gs, NF)
REDUCE'II'IN₂(sequent₂(cons₂(p₁(V), Fs), Gs), sequent₂(Left, Right)) -> REDUCE'II'IN₂(sequent₂(Fs, Gs), sequent₂(cons₂(p₁(V), Left), Right))

The remaining pairs can at least be oriented weakly.

REDUCE'II'IN₂(sequent₂(cons₂(x'2d₁(F1), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(F1, Gs)), NF)
REDUCE'II'IN₂(sequent₂(cons₂(x'2a₂(F1, F2), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(F1, cons₂(F2, Fs)), Gs), NF)
REDUCE'II'IN₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2d₁(G1), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(G1, Fs), Gs), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(iff₂(A, B), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Gs)), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2b₂(G1, G2), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(G1, cons₂(G2, Gs))), NF)
REDUCE'II'IN₂(sequent₂(cons₂(iff₂(A, B), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Fs), Gs), NF)
U'12'1₅(reduce'ii'out, Fs, G2, Gs, NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(G2, Gs)), NF)

Used ordering: Polynomial Order [17,21] with Interpretation:

POL( u'13'1₁(x₁) ) = max{0, -3}

POL( u'6'2₁(x₁) ) = max{0, -3}

POL( u'15'1₁(x₁) ) = 0

POL( u'7'1₁(x₁) ) = max{0, -3}

POL( REDUCE'II'IN₂(x₁, x₂) ) = x₁

POL( u'5'1₁(x₁) ) = max{0, -3}

POL( x'2a₂(x₁, x₂) ) = x₁ + x₂ + 1

POL( U'12'1₅(x₁, ..., x₅) ) = 2x₂ + 2x₃ + 2x₄ + 1

POL( u'11'1₁(x₁) ) = 2

POL( intersect'ii'in₂(x₁, x₂) ) = max{0, -3}

POL( u'6'1₅(x₁, ..., x₅) ) = max{0, 3x₃ + x₄ + x₅ - 1}

POL( u'1'1₁(x₁) ) = max{0, x₁ - 1}

POL( cons₂(x₁, x₂) ) = x₁ + x₂ + 1

POL( u'12'2₁(x₁) ) = 0

POL( iff₂(x₁, x₂) ) = 3x₁ + 3x₂ + 3

POL( u'12'1₅(x₁, ..., x₅) ) = max{0, -3}

POL( if₂(x₁, x₂) ) = x₁ + 2x₂ + 1

POL( u'8'1₁(x₁) ) = max{0, 2x₁ - 2}

POL( sequent₂(x₁, x₂) ) = max{0, 2x₁ + 2x₂ - 1}

POL( x'2d₁(x₁) ) = x₁

POL( u'4'1₁(x₁) ) = 1

POL( u'10'1₁(x₁) ) = 2

POL( intersect'ii'out ) = 2

POL( u'3'1₁(x₁) ) = max{0, x₁ - 3}

POL( p₁(x₁) ) = 3

POL( u'2'1₁(x₁) ) = 3

POL( reduce'ii'in₂(x₁, x₂) ) = 2x₁ + 2

POL( nil ) = 1

POL( reduce'ii'out ) = 1

POL( U'6'1₅(x₁, ..., x₅) ) = 2x₂ + 2x₃ + 2x₄ + 2

POL( x'2b₂(x₁, x₂) ) = 2x₁ + x₂ + 1

POL( u'14'1₁(x₁) ) = 0

POL( u'9'1₁(x₁) ) = max{0, 3x₁ - 3}

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2d₁(G1), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(G1, Fs), Gs), NF)
REDUCE'II'IN₂(sequent₂(cons₂(x'2d₁(F1), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(F1, Gs)), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(iff₂(A, B), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Gs)), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2b₂(G1, G2), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(G1, cons₂(G2, Gs))), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF)
REDUCE'II'IN₂(sequent₂(cons₂(x'2a₂(F1, F2), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(F1, cons₂(F2, Fs)), Gs), NF)
REDUCE'II'IN₂(sequent₂(cons₂(iff₂(A, B), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Fs), Gs), NF)
REDUCE'II'IN₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF)
U'12'1₅(reduce'ii'out, Fs, G2, Gs, NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(G2, Gs)), NF)

The TRS R consists of the following rules:

intersect'ii'in₂(cons₂(X, X0), cons₂(X, X1)) -> intersect'ii'out
intersect'ii'in₂(Xs, cons₂(X0, Ys)) -> u'1'1₁(intersect'ii'in₂(Xs, Ys))
u'1'1₁(intersect'ii'out) -> intersect'ii'out
intersect'ii'in₂(cons₂(X0, Xs), Ys) -> u'2'1₁(intersect'ii'in₂(Xs, Ys))
u'2'1₁(intersect'ii'out) -> intersect'ii'out
reduce'ii'in₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> u'3'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF))
u'3'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(iff₂(A, B), Fs), Gs), NF) -> u'4'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Fs), Gs), NF))
u'4'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2a₂(F1, F2), Fs), Gs), NF) -> u'5'1₁(reduce'ii'in₂(sequent₂(cons₂(F1, cons₂(F2, Fs)), Gs), NF))
u'5'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2b₂(F1, F2), Fs), Gs), NF) -> u'6'1₅(reduce'ii'in₂(sequent₂(cons₂(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1₅(reduce'ii'out, F2, Fs, Gs, NF) -> u'6'2₁(reduce'ii'in₂(sequent₂(cons₂(F2, Fs), Gs), NF))
u'6'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2d₁(F1), Fs), Gs), NF) -> u'7'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(F1, Gs)), NF))
u'7'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> u'8'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF))
u'8'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(iff₂(A, B), Gs)), NF) -> u'9'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Gs)), NF))
u'9'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(p₁(V), Fs), Gs), sequent₂(Left, Right)) -> u'10'1₁(reduce'ii'in₂(sequent₂(Fs, Gs), sequent₂(cons₂(p₁(V), Left), Right)))
u'10'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(G1, G2), Gs)), NF) -> u'11'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, cons₂(G2, Gs))), NF))
u'11'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(G1, G2), Gs)), NF) -> u'12'1₅(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1₅(reduce'ii'out, Fs, G2, Gs, NF) -> u'12'2₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G2, Gs)), NF))
u'12'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2d₁(G1), Gs)), NF) -> u'13'1₁(reduce'ii'in₂(sequent₂(cons₂(G1, Fs), Gs), NF))
u'13'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, cons₂(p₁(V), Gs)), sequent₂(Left, Right)) -> u'14'1₁(reduce'ii'in₂(sequent₂(nil, Gs), sequent₂(Left, cons₂(p₁(V), Right))))
u'14'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, nil), sequent₂(F1, F2)) -> u'15'1₁(intersect'ii'in₂(F1, F2))
u'15'1₁(intersect'ii'out) -> reduce'ii'out
tautology'i'in₁(F) -> u'16'1₁(reduce'ii'in₂(sequent₂(nil, cons₂(F, nil)), sequent₂(nil, nil)))
u'16'1₁(reduce'ii'out) -> tautology'i'out

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 1 SCC with 1 less node.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ DependencyGraphProof

                  ↳ QDP

                    ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2d₁(G1), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(G1, Fs), Gs), NF)
REDUCE'II'IN₂(sequent₂(cons₂(x'2d₁(F1), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(F1, Gs)), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(iff₂(A, B), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Gs)), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2b₂(G1, G2), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(G1, cons₂(G2, Gs))), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF)
REDUCE'II'IN₂(sequent₂(cons₂(x'2a₂(F1, F2), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(F1, cons₂(F2, Fs)), Gs), NF)
REDUCE'II'IN₂(sequent₂(cons₂(iff₂(A, B), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Fs), Gs), NF)
REDUCE'II'IN₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF)

The TRS R consists of the following rules:

intersect'ii'in₂(cons₂(X, X0), cons₂(X, X1)) -> intersect'ii'out
intersect'ii'in₂(Xs, cons₂(X0, Ys)) -> u'1'1₁(intersect'ii'in₂(Xs, Ys))
u'1'1₁(intersect'ii'out) -> intersect'ii'out
intersect'ii'in₂(cons₂(X0, Xs), Ys) -> u'2'1₁(intersect'ii'in₂(Xs, Ys))
u'2'1₁(intersect'ii'out) -> intersect'ii'out
reduce'ii'in₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> u'3'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF))
u'3'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(iff₂(A, B), Fs), Gs), NF) -> u'4'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Fs), Gs), NF))
u'4'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2a₂(F1, F2), Fs), Gs), NF) -> u'5'1₁(reduce'ii'in₂(sequent₂(cons₂(F1, cons₂(F2, Fs)), Gs), NF))
u'5'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2b₂(F1, F2), Fs), Gs), NF) -> u'6'1₅(reduce'ii'in₂(sequent₂(cons₂(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1₅(reduce'ii'out, F2, Fs, Gs, NF) -> u'6'2₁(reduce'ii'in₂(sequent₂(cons₂(F2, Fs), Gs), NF))
u'6'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2d₁(F1), Fs), Gs), NF) -> u'7'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(F1, Gs)), NF))
u'7'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> u'8'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF))
u'8'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(iff₂(A, B), Gs)), NF) -> u'9'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Gs)), NF))
u'9'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(p₁(V), Fs), Gs), sequent₂(Left, Right)) -> u'10'1₁(reduce'ii'in₂(sequent₂(Fs, Gs), sequent₂(cons₂(p₁(V), Left), Right)))
u'10'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(G1, G2), Gs)), NF) -> u'11'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, cons₂(G2, Gs))), NF))
u'11'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(G1, G2), Gs)), NF) -> u'12'1₅(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1₅(reduce'ii'out, Fs, G2, Gs, NF) -> u'12'2₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G2, Gs)), NF))
u'12'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2d₁(G1), Gs)), NF) -> u'13'1₁(reduce'ii'in₂(sequent₂(cons₂(G1, Fs), Gs), NF))
u'13'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, cons₂(p₁(V), Gs)), sequent₂(Left, Right)) -> u'14'1₁(reduce'ii'in₂(sequent₂(nil, Gs), sequent₂(Left, cons₂(p₁(V), Right))))
u'14'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, nil), sequent₂(F1, F2)) -> u'15'1₁(intersect'ii'in₂(F1, F2))
u'15'1₁(intersect'ii'out) -> reduce'ii'out
tautology'i'in₁(F) -> u'16'1₁(reduce'ii'in₂(sequent₂(nil, cons₂(F, nil)), sequent₂(nil, nil)))
u'16'1₁(reduce'ii'out) -> tautology'i'out

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2b₂(G1, G2), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(G1, cons₂(G2, Gs))), NF)
REDUCE'II'IN₂(sequent₂(cons₂(x'2a₂(F1, F2), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(F1, cons₂(F2, Fs)), Gs), NF)

The remaining pairs can at least be oriented weakly.

REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2d₁(G1), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(G1, Fs), Gs), NF)
REDUCE'II'IN₂(sequent₂(cons₂(x'2d₁(F1), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(F1, Gs)), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(iff₂(A, B), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Gs)), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF)
REDUCE'II'IN₂(sequent₂(cons₂(iff₂(A, B), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Fs), Gs), NF)
REDUCE'II'IN₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF)

Used ordering: Polynomial Order [17,21] with Interpretation:

POL( if₂(x₁, x₂) ) = x₁ + 2x₂ + 1

POL( REDUCE'II'IN₂(x₁, x₂) ) = 2x₁ + 3x₂

POL( x'2d₁(x₁) ) = 2x₁

POL( sequent₂(x₁, x₂) ) = max{0, 2x₁ + 2x₂ - 2}

POL( x'2a₂(x₁, x₂) ) = x₁ + x₂ + 1

POL( x'2b₂(x₁, x₂) ) = x₁ + x₂ + 1

POL( cons₂(x₁, x₂) ) = 2x₁ + x₂ + 1

POL( iff₂(x₁, x₂) ) = 3x₁ + 3x₂ + 3

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ DependencyGraphProof

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2d₁(G1), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(G1, Fs), Gs), NF)
REDUCE'II'IN₂(sequent₂(cons₂(x'2d₁(F1), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(F1, Gs)), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(iff₂(A, B), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Gs)), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF)
REDUCE'II'IN₂(sequent₂(cons₂(iff₂(A, B), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Fs), Gs), NF)
REDUCE'II'IN₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF)

The TRS R consists of the following rules:

intersect'ii'in₂(cons₂(X, X0), cons₂(X, X1)) -> intersect'ii'out
intersect'ii'in₂(Xs, cons₂(X0, Ys)) -> u'1'1₁(intersect'ii'in₂(Xs, Ys))
u'1'1₁(intersect'ii'out) -> intersect'ii'out
intersect'ii'in₂(cons₂(X0, Xs), Ys) -> u'2'1₁(intersect'ii'in₂(Xs, Ys))
u'2'1₁(intersect'ii'out) -> intersect'ii'out
reduce'ii'in₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> u'3'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF))
u'3'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(iff₂(A, B), Fs), Gs), NF) -> u'4'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Fs), Gs), NF))
u'4'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2a₂(F1, F2), Fs), Gs), NF) -> u'5'1₁(reduce'ii'in₂(sequent₂(cons₂(F1, cons₂(F2, Fs)), Gs), NF))
u'5'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2b₂(F1, F2), Fs), Gs), NF) -> u'6'1₅(reduce'ii'in₂(sequent₂(cons₂(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1₅(reduce'ii'out, F2, Fs, Gs, NF) -> u'6'2₁(reduce'ii'in₂(sequent₂(cons₂(F2, Fs), Gs), NF))
u'6'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2d₁(F1), Fs), Gs), NF) -> u'7'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(F1, Gs)), NF))
u'7'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> u'8'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF))
u'8'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(iff₂(A, B), Gs)), NF) -> u'9'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Gs)), NF))
u'9'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(p₁(V), Fs), Gs), sequent₂(Left, Right)) -> u'10'1₁(reduce'ii'in₂(sequent₂(Fs, Gs), sequent₂(cons₂(p₁(V), Left), Right)))
u'10'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(G1, G2), Gs)), NF) -> u'11'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, cons₂(G2, Gs))), NF))
u'11'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(G1, G2), Gs)), NF) -> u'12'1₅(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1₅(reduce'ii'out, Fs, G2, Gs, NF) -> u'12'2₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G2, Gs)), NF))
u'12'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2d₁(G1), Gs)), NF) -> u'13'1₁(reduce'ii'in₂(sequent₂(cons₂(G1, Fs), Gs), NF))
u'13'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, cons₂(p₁(V), Gs)), sequent₂(Left, Right)) -> u'14'1₁(reduce'ii'in₂(sequent₂(nil, Gs), sequent₂(Left, cons₂(p₁(V), Right))))
u'14'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, nil), sequent₂(F1, F2)) -> u'15'1₁(intersect'ii'in₂(F1, F2))
u'15'1₁(intersect'ii'out) -> reduce'ii'out
tautology'i'in₁(F) -> u'16'1₁(reduce'ii'in₂(sequent₂(nil, cons₂(F, nil)), sequent₂(nil, nil)))
u'16'1₁(reduce'ii'out) -> tautology'i'out

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2d₁(G1), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(G1, Fs), Gs), NF)
REDUCE'II'IN₂(sequent₂(cons₂(x'2d₁(F1), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(F1, Gs)), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(iff₂(A, B), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Gs)), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF)
REDUCE'II'IN₂(sequent₂(cons₂(iff₂(A, B), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Fs), Gs), NF)
REDUCE'II'IN₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial Order [17,21] with Interpretation:

POL( if₂(x₁, x₂) ) = x₁ + x₂ + 2

POL( REDUCE'II'IN₂(x₁, x₂) ) = max{0, x₁ + 3x₂ - 3}

POL( x'2d₁(x₁) ) = 2x₁ + 2

POL( sequent₂(x₁, x₂) ) = 2x₁ + 2x₂ + 2

POL( x'2a₂(x₁, x₂) ) = max{0, -3}

POL( x'2b₂(x₁, x₂) ) = x₂

POL( cons₂(x₁, x₂) ) = 2x₁ + x₂

POL( iff₂(x₁, x₂) ) = x₁ + 3x₂ + 2

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ DependencyGraphProof

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

intersect'ii'in₂(cons₂(X, X0), cons₂(X, X1)) -> intersect'ii'out
intersect'ii'in₂(Xs, cons₂(X0, Ys)) -> u'1'1₁(intersect'ii'in₂(Xs, Ys))
u'1'1₁(intersect'ii'out) -> intersect'ii'out
intersect'ii'in₂(cons₂(X0, Xs), Ys) -> u'2'1₁(intersect'ii'in₂(Xs, Ys))
u'2'1₁(intersect'ii'out) -> intersect'ii'out
reduce'ii'in₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> u'3'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF))
u'3'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(iff₂(A, B), Fs), Gs), NF) -> u'4'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Fs), Gs), NF))
u'4'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2a₂(F1, F2), Fs), Gs), NF) -> u'5'1₁(reduce'ii'in₂(sequent₂(cons₂(F1, cons₂(F2, Fs)), Gs), NF))
u'5'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2b₂(F1, F2), Fs), Gs), NF) -> u'6'1₅(reduce'ii'in₂(sequent₂(cons₂(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1₅(reduce'ii'out, F2, Fs, Gs, NF) -> u'6'2₁(reduce'ii'in₂(sequent₂(cons₂(F2, Fs), Gs), NF))
u'6'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2d₁(F1), Fs), Gs), NF) -> u'7'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(F1, Gs)), NF))
u'7'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> u'8'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF))
u'8'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(iff₂(A, B), Gs)), NF) -> u'9'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Gs)), NF))
u'9'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(p₁(V), Fs), Gs), sequent₂(Left, Right)) -> u'10'1₁(reduce'ii'in₂(sequent₂(Fs, Gs), sequent₂(cons₂(p₁(V), Left), Right)))
u'10'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(G1, G2), Gs)), NF) -> u'11'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, cons₂(G2, Gs))), NF))
u'11'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(G1, G2), Gs)), NF) -> u'12'1₅(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1₅(reduce'ii'out, Fs, G2, Gs, NF) -> u'12'2₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G2, Gs)), NF))
u'12'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2d₁(G1), Gs)), NF) -> u'13'1₁(reduce'ii'in₂(sequent₂(cons₂(G1, Fs), Gs), NF))
u'13'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, cons₂(p₁(V), Gs)), sequent₂(Left, Right)) -> u'14'1₁(reduce'ii'in₂(sequent₂(nil, Gs), sequent₂(Left, cons₂(p₁(V), Right))))
u'14'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, nil), sequent₂(F1, F2)) -> u'15'1₁(intersect'ii'in₂(F1, F2))
u'15'1₁(intersect'ii'out) -> reduce'ii'out
tautology'i'in₁(F) -> u'16'1₁(reduce'ii'in₂(sequent₂(nil, cons₂(F, nil)), sequent₂(nil, nil)))
u'16'1₁(reduce'ii'out) -> tautology'i'out

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.